$\forall$$M$:MsgA, $k$:Knd, $x$:Id. $M$.rframe($k$ reads $x$) $\in$ Prop